T:Type, R:(TT), x:T, L:(T List).
sorted-by(R;[x / L])  (sorted-by(R;L) & (zL. R(x,z))) 

latex

Definitions

f(a), x:AB(x), x:A. B(x), ||as||, n+m, P  Q, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , {i..j}, Type, type List, xL. P(x), a < b, x. t(x), t  T, s = t, , Void, x:A  B(x), (x  l), x.A(x), l[i], A List, [car / cdr], #$n, P  Q, P  Q, sorted-by(R;L), n - m, , T, True, hd(l), i <z j, i z j, |g|, S  T, A c B, x:A. B(x), SQType(T), s ~ t, {T}, left + right, P  Q, Dec(P), Atom, , b, x,y:A//B(x;y), b | a, a ~ b, |p|, a  b, a <p b, a < b, x f y, |r|, (xL.P(x)), Unit, , -n

Lemmas

select member, true wf, decidable int equal, guard wf, squash wf, nat wf, member wf, le wf, iff wf, rev implies wf, select cons tl, length wf1, int seg wf, select wf, l all wf2, l member wf, l all wf